/******************************************************************************

    Copyright (C) 2006 - 2010 Alessio Stalla (alessiostalla@gmail.com)

    This file is part of PrettyProlog.

    PrettyProlog is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 3 of the License, or
    (at your option) any later version.

    PrettyProlog is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with PrettyProlog; if not, write to the Free Software
    Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA

    See the file COPYING for further details.

 *****************************************************************************/

package prettyprolog.engine;

import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Vector;

import prettyprolog.datatypes.Callable;
import prettyprolog.datatypes.CharString;
import prettyprolog.datatypes.Cons;
import prettyprolog.datatypes.Constant;
import prettyprolog.datatypes.JavaObject;
import prettyprolog.datatypes.Namespace;
import prettyprolog.datatypes.Nil;
import prettyprolog.datatypes.Real;
import prettyprolog.datatypes.Substitution;
import prettyprolog.datatypes.Term;
import prettyprolog.datatypes.Variable;

/**
 * This class provides a single public method, {@link #unify(Term, Term)
 * unify(Term, Term)}, which is used to unify two terms.
 */
public class UnificationAlgorithm implements Unifier {
	
	private final Map<Class<?>, Map<Class<?>, Unifier>> unifiers = new HashMap<Class<?>, Map<Class<?>,Unifier>>(); //TODO classmap
	
	public void setUnifier(Class<?> t1, Class<?> t2, Unifier u) {
		synchronized (unifiers) {
			setUnifierAux(t1, t2, u);
			if(t1 != t2) {
				setUnifierAux(t2, t1, new InverseUnifier(u));
			}
		}
	}

	protected void setUnifierAux(Class<?> t1, Class<?> t2, Unifier u) {
		Map<Class<?>, Unifier> map = unifiers.get(t1);
		if(map == null) {
			map = new HashMap<Class<?>, Unifier>();
			unifiers.put(t1, map);
		}
		map.put(t2, u);
	}
	
	public Unifier getUnifier(Class<?> t1, Class<?> t2) { //Non synchronized: all unificationAlgorithm must be set before starting to use this
		Map<Class<?>, Unifier> map = unifiers.get(t1);
		if(map != null) {
			return map.get(t2);
		} else {
			return null;
		}
	}
	
	public Substitution unify(Term t1, Term t2) {
		if(t1 == null || t2 == null) {
			return null;
		}
		Unifier u = getUnifier(t1.getClass(), t2.getClass());
		if(u != null) {
			return u.unify(t1, t2, this);
		} else if(t1.equals(t2)) {
			return new Substitution();
		} else {
			return null;
		}
	}
	
	public UnificationAlgorithm() {
		setUnifier(Variable.class, Variable.class, new VariableVariableUnifier());
		setUnifier(Variable.class, Callable.class, new VariableCompositeUnifier());
		setUnifier(Variable.class, Cons.class, new VariableCompositeUnifier());
		setUnifier(Variable.class, Real.class, new VariableAtomUnifier());
		setUnifier(Variable.class, Constant.class, new VariableAtomUnifier());
		setUnifier(Variable.class, CharString.class, new VariableAtomUnifier());
		setUnifier(Variable.class, JavaObject.class, new VariableAtomUnifier());
		setUnifier(Variable.class, Nil.class, new VariableAtomUnifier());
		setUnifier(Variable.class, Namespace.class, new VariableAtomUnifier());
				
		setUnifier(Callable.class, Callable.class, new CallableCallableUnifier());
		setUnifier(Callable.class, Constant.class, new CallableCallableUnifier());
		
		setUnifier(Cons.class, Cons.class, new ConsConsUnifier());
	}

	/** Var --> var */
	protected static class VariableVariableUnifier implements Unifier {
		public Substitution unify(Term v1, Term v2, Unifier u) {
			if(((Variable) v1).isAnonymous() || ((Variable) v2).isAnonymous()) {
				return new Substitution();
			} 
			Substitution subst = new Substitution();
			subst.putMapping((Variable) v1, (Variable) v2);
			return subst;
		}
	}

	/** Var --> { Callable, Cons } */
	protected static class VariableCompositeUnifier implements Unifier {
		public Substitution unify(Term v, Term c, Unifier u) {
			if(((Variable) v).isAnonymous()) {
				return new Substitution();
			}
			Substitution subst = null;
			if (!c.contains(v, true)) {
				subst = new Substitution();
				subst.putMapping((Variable) v, c);
			}
			return subst;
		}
	}

	/** Var --> { Real, String } */
	protected static class VariableAtomUnifier implements Unifier {
		public Substitution unify(Term v, Term x, Unifier u) {
			if(((Variable) v).isAnonymous()) {
				return new Substitution();
			}
			Substitution subst = new Substitution();
			subst.putMapping((Variable) v, x);
			return subst;
		}
	}

	/** Callable --> Callable */
	protected static class CallableCallableUnifier implements Unifier {
		public Substitution unify(Term t1, Term t2, Unifier u) {
			Callable c1 = (Callable) t1, c2 = (Callable) t2;
			if ((c1.getSymbol() != null) && (c2.getSymbol() != null)) {
				if (!c1.getSymbol().equals(c2.getSymbol()))
					return null;
				if (c1.getArgCount() != c2.getArgCount())
					return null;
			} else if ((c1.getSymbol() != null) || (c2.getSymbol() != null))
				return null;
			// Unify two tuples (Callables with null Symbol) or
			// two Callables with non-null symbols and equal-sized
			// argument lists
			Substitution subst = new Substitution();
			List<Term> shorter = new Vector<Term>(c1.getArgs());
			List<Term> longer = new Vector<Term>(c2.getArgs());
			int min = c1.getArgCount();
			int max = c2.getArgCount();
			if (min > max) {
				// Swap max & min
				int tmp = min;
				min = max;
				max = tmp;
				// Swap longer & shorter
				List<Term> tmplist = shorter;
				shorter = longer;
				longer = tmplist;
			}
			int cnt = min;
			// This is because if lengths are different the last term gets
			// treated specially
			if (min != max)
				cnt--;
			// Unify arg-by-arg and compose the resulting Substitutions
			for (int i = 0; i < cnt; i++) {
				Substitution tmp_subst = u.unify(shorter.get(i), longer.get(i), u);
				if (tmp_subst == null)
					return null;
				for (int j = i + 1; j < cnt; j++) {
					shorter.set(j, shorter.get(j).apply(tmp_subst));
					longer.set(j, longer.get(j).apply(tmp_subst));
				}
				subst = subst.compose(tmp_subst);
			}
	
			// Allow something as (X, Y) = (1, 2, 3)
			// producing X = 1 (code above)
			// and Y = (2, 3) (code below)
			if ((min != max) && (min > 0)) {
				Callable rest = new Callable(null, longer.subList(min - 1, max));
				Substitution tmp_subst = u.unify(shorter.get(min - 1), rest, u);
				if (tmp_subst == null)
					return null;
				subst = subst.compose(tmp_subst);
			}
			return subst;
		}
	}

	/** Cons --> Cons */
	protected static class ConsConsUnifier implements Unifier {
		public Substitution unify(Term t1, Term t2, Unifier u) {
			Cons c1 = (Cons) t1, c2 = (Cons) t2;
			Substitution subst = u.unify(c1.car(), c2.car(), u);
			if (subst == null) {
				return null;
			}
			// Applico ai cdr la sostituzione che unifica i car
			Term cdr1 = c1.cdr().apply(subst);
			Term cdr2 = c2.cdr().apply(subst);
			// Vado avanti ricorsivamente
			Substitution tmp = u.unify(cdr1, cdr2, u);
			if (tmp == null) {
				return null;
			}
			if (!tmp.isEmpty()) {
				subst = tmp.compose(subst);
			}
			// ho finito
			return subst;
		}
	}
	
	protected static class InverseUnifier implements Unifier {
		private final Unifier inv;
		protected InverseUnifier(Unifier inv) { this.inv = inv; }
		public Substitution unify(Term t1, Term t2, Unifier u) {
			return inv.unify(t2, t1, u);
		}
	}

	public Substitution unify(Term t1, Term t2, Unifier unifier) {
		return unify(t1, t2);
	}

}